Nuprl Lemma : contravariance-variant
11,40
postcript
pdf
A
,
A'
:Type{i},
B
:Type{i'},
f
:(
A
B
). (
A'
r
A
)
(
f
A'
B
)
latex
Definitions
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
S
T
,
Type
,
suptype(
S
;
T
)
,
P
Q
origin
A, A':Type{i}, B:Type{i'}, f:(A
B). (A' 
r A) 
(f 
A'B) A, A':Type{i}, B:Type{i'}, f:(AB). (A' r A) (f A'B) TB(x)x:A. B(x) T Q